YES 2.101 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ IFR

mainModule List
  ((delete :: (Eq a, Eq b) => (a,b ->  [(a,b)]  ->  [(a,b)]) :: (Eq b, Eq a) => (a,b ->  [(a,b)]  ->  [(a,b)])

module List where
  import qualified Maybe
import qualified Prelude

  delete :: Eq a => a  ->  [a ->  [a]
delete deleteBy (==)

  deleteBy :: (a  ->  a  ->  Bool ->  a  ->  [a ->  [a]
deleteBy _ _ [] []
deleteBy eq x (y : ys if x `eq` y then ys else y : deleteBy eq x ys


module Maybe where
  import qualified List
import qualified Prelude



If Reductions:
The following If expression
if eq x y then ys else y : deleteBy eq x ys

is transformed to
deleteBy0 ys y eq x True = ys
deleteBy0 ys y eq x False = y : deleteBy eq x ys



↳ HASKELL
  ↳ IFR
HASKELL
      ↳ BR

mainModule List
  ((delete :: (Eq b, Eq a) => (b,a ->  [(b,a)]  ->  [(b,a)]) :: (Eq a, Eq b) => (b,a ->  [(b,a)]  ->  [(b,a)])

module List where
  import qualified Maybe
import qualified Prelude

  delete :: Eq a => a  ->  [a ->  [a]
delete deleteBy (==)

  deleteBy :: (a  ->  a  ->  Bool ->  a  ->  [a ->  [a]
deleteBy _ _ [] []
deleteBy eq x (y : ysdeleteBy0 ys y eq x (x `eq` y)

  
deleteBy0 ys y eq x True ys
deleteBy0 ys y eq x False y : deleteBy eq x ys


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
HASKELL
          ↳ COR

mainModule List
  ((delete :: (Eq b, Eq a) => (a,b ->  [(a,b)]  ->  [(a,b)]) :: (Eq b, Eq a) => (a,b ->  [(a,b)]  ->  [(a,b)])

module List where
  import qualified Maybe
import qualified Prelude

  delete :: Eq a => a  ->  [a ->  [a]
delete deleteBy (==)

  deleteBy :: (a  ->  a  ->  Bool ->  a  ->  [a ->  [a]
deleteBy vw vx [] []
deleteBy eq x (y : ysdeleteBy0 ys y eq x (x `eq` y)

  
deleteBy0 ys y eq x True ys
deleteBy0 ys y eq x False y : deleteBy eq x ys


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
HASKELL
              ↳ Narrow

mainModule List
  (delete :: (Eq a, Eq b) => (a,b ->  [(a,b)]  ->  [(a,b)])

module List where
  import qualified Maybe
import qualified Prelude

  delete :: Eq a => a  ->  [a ->  [a]
delete deleteBy (==)

  deleteBy :: (a  ->  a  ->  Bool ->  a  ->  [a ->  [a]
deleteBy vw vx [] []
deleteBy eq x (y : ysdeleteBy0 ys y eq x (x `eq` y)

  
deleteBy0 ys y eq x True ys
deleteBy0 ys y eq x False y : deleteBy eq x ys


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xy4400), Succ(xy4010000)) → new_primPlusNat(xy4400, xy4010000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xy31000), Succ(xy401000)) → new_primMulNat(xy31000, Succ(xy401000))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xy3100), Succ(xy40100)) → new_primEqNat(xy3100, xy40100)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs2(Left(xy310), Left(xy4010), app(ty_[], gb), gc) → new_esEs(xy310, xy4010, gb)
new_esEs(:(xy310, xy311), :(xy4010, xy4011), app(app(ty_@2, bc), bd)) → new_esEs0(xy310, xy4010, bc, bd)
new_esEs2(Right(xy310), Right(xy4010), hd, app(ty_[], he)) → new_esEs(xy310, xy4010, he)
new_esEs3(@3(xy310, xy311, xy312), @3(xy4010, xy4011, xy4012), app(app(ty_Either, bdg), bdh), bag, bcb) → new_esEs2(xy310, xy4010, bdg, bdh)
new_esEs3(@3(xy310, xy311, xy312), @3(xy4010, xy4011, xy4012), baf, bag, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs3(xy312, xy4012, bbf, bbg, bbh)
new_esEs2(Left(xy310), Left(xy4010), app(app(ty_@2, gd), ge), gc) → new_esEs0(xy310, xy4010, gd, ge)
new_esEs3(@3(xy310, xy311, xy312), @3(xy4010, xy4011, xy4012), baf, bag, app(ty_[], bah)) → new_esEs(xy312, xy4012, bah)
new_esEs3(@3(xy310, xy311, xy312), @3(xy4010, xy4011, xy4012), baf, bag, app(ty_Maybe, bbc)) → new_esEs1(xy312, xy4012, bbc)
new_esEs0(@2(xy310, xy311), @2(xy4010, xy4011), app(app(ty_Either, ec), ed), dg) → new_esEs2(xy310, xy4010, ec, ed)
new_esEs3(@3(xy310, xy311, xy312), @3(xy4010, xy4011, xy4012), app(app(ty_@2, bdd), bde), bag, bcb) → new_esEs0(xy310, xy4010, bdd, bde)
new_esEs(:(xy310, xy311), :(xy4010, xy4011), app(app(app(ty_@3, bh), ca), cb)) → new_esEs3(xy310, xy4010, bh, ca, cb)
new_esEs3(@3(xy310, xy311, xy312), @3(xy4010, xy4011, xy4012), app(ty_[], bdc), bag, bcb) → new_esEs(xy310, xy4010, bdc)
new_esEs3(@3(xy310, xy311, xy312), @3(xy4010, xy4011, xy4012), baf, app(app(ty_Either, bcf), bcg), bcb) → new_esEs2(xy311, xy4011, bcf, bcg)
new_esEs1(Just(xy310), Just(xy4010), app(app(app(ty_@3, fg), fh), ga)) → new_esEs3(xy310, xy4010, fg, fh, ga)
new_esEs3(@3(xy310, xy311, xy312), @3(xy4010, xy4011, xy4012), baf, app(ty_[], bca), bcb) → new_esEs(xy311, xy4011, bca)
new_esEs2(Left(xy310), Left(xy4010), app(app(ty_Either, gg), gh), gc) → new_esEs2(xy310, xy4010, gg, gh)
new_esEs2(Left(xy310), Left(xy4010), app(app(app(ty_@3, ha), hb), hc), gc) → new_esEs3(xy310, xy4010, ha, hb, hc)
new_esEs3(@3(xy310, xy311, xy312), @3(xy4010, xy4011, xy4012), app(ty_Maybe, bdf), bag, bcb) → new_esEs1(xy310, xy4010, bdf)
new_esEs3(@3(xy310, xy311, xy312), @3(xy4010, xy4011, xy4012), baf, app(app(ty_@2, bcc), bcd), bcb) → new_esEs0(xy311, xy4011, bcc, bcd)
new_esEs2(Right(xy310), Right(xy4010), hd, app(app(ty_@2, hf), hg)) → new_esEs0(xy310, xy4010, hf, hg)
new_esEs0(@2(xy310, xy311), @2(xy4010, xy4011), cc, app(ty_[], cd)) → new_esEs(xy311, xy4011, cd)
new_esEs1(Just(xy310), Just(xy4010), app(app(ty_@2, fa), fb)) → new_esEs0(xy310, xy4010, fa, fb)
new_esEs2(Left(xy310), Left(xy4010), app(ty_Maybe, gf), gc) → new_esEs1(xy310, xy4010, gf)
new_esEs1(Just(xy310), Just(xy4010), app(app(ty_Either, fd), ff)) → new_esEs2(xy310, xy4010, fd, ff)
new_esEs3(@3(xy310, xy311, xy312), @3(xy4010, xy4011, xy4012), baf, bag, app(app(ty_Either, bbd), bbe)) → new_esEs2(xy312, xy4012, bbd, bbe)
new_esEs1(Just(xy310), Just(xy4010), app(ty_[], eh)) → new_esEs(xy310, xy4010, eh)
new_esEs3(@3(xy310, xy311, xy312), @3(xy4010, xy4011, xy4012), baf, app(app(app(ty_@3, bch), bda), bdb), bcb) → new_esEs3(xy311, xy4011, bch, bda, bdb)
new_esEs(:(xy310, xy311), :(xy4010, xy4011), ba) → new_esEs(xy311, xy4011, ba)
new_esEs(:(xy310, xy311), :(xy4010, xy4011), app(app(ty_Either, bf), bg)) → new_esEs2(xy310, xy4010, bf, bg)
new_esEs0(@2(xy310, xy311), @2(xy4010, xy4011), app(app(app(ty_@3, ee), ef), eg), dg) → new_esEs3(xy310, xy4010, ee, ef, eg)
new_esEs0(@2(xy310, xy311), @2(xy4010, xy4011), cc, app(app(ty_Either, da), db)) → new_esEs2(xy311, xy4011, da, db)
new_esEs2(Right(xy310), Right(xy4010), hd, app(app(ty_Either, baa), bab)) → new_esEs2(xy310, xy4010, baa, bab)
new_esEs1(Just(xy310), Just(xy4010), app(ty_Maybe, fc)) → new_esEs1(xy310, xy4010, fc)
new_esEs2(Right(xy310), Right(xy4010), hd, app(ty_Maybe, hh)) → new_esEs1(xy310, xy4010, hh)
new_esEs0(@2(xy310, xy311), @2(xy4010, xy4011), app(app(ty_@2, dh), ea), dg) → new_esEs0(xy310, xy4010, dh, ea)
new_esEs0(@2(xy310, xy311), @2(xy4010, xy4011), app(ty_[], df), dg) → new_esEs(xy310, xy4010, df)
new_esEs0(@2(xy310, xy311), @2(xy4010, xy4011), cc, app(ty_Maybe, cg)) → new_esEs1(xy311, xy4011, cg)
new_esEs0(@2(xy310, xy311), @2(xy4010, xy4011), app(ty_Maybe, eb), dg) → new_esEs1(xy310, xy4010, eb)
new_esEs0(@2(xy310, xy311), @2(xy4010, xy4011), cc, app(app(ty_@2, ce), cf)) → new_esEs0(xy311, xy4011, ce, cf)
new_esEs2(Right(xy310), Right(xy4010), hd, app(app(app(ty_@3, bac), bad), bae)) → new_esEs3(xy310, xy4010, bac, bad, bae)
new_esEs3(@3(xy310, xy311, xy312), @3(xy4010, xy4011, xy4012), baf, bag, app(app(ty_@2, bba), bbb)) → new_esEs0(xy312, xy4012, bba, bbb)
new_esEs0(@2(xy310, xy311), @2(xy4010, xy4011), cc, app(app(app(ty_@3, dc), dd), de)) → new_esEs3(xy311, xy4011, dc, dd, de)
new_esEs(:(xy310, xy311), :(xy4010, xy4011), app(ty_[], bb)) → new_esEs(xy310, xy4010, bb)
new_esEs3(@3(xy310, xy311, xy312), @3(xy4010, xy4011, xy4012), app(app(app(ty_@3, bea), beb), bec), bag, bcb) → new_esEs3(xy310, xy4010, bea, beb, bec)
new_esEs(:(xy310, xy311), :(xy4010, xy4011), app(ty_Maybe, be)) → new_esEs1(xy310, xy4010, be)
new_esEs3(@3(xy310, xy311, xy312), @3(xy4010, xy4011, xy4012), baf, app(ty_Maybe, bce), bcb) → new_esEs1(xy311, xy4011, bce)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_deleteBy(@2(xy30, xy31), :(@2(xy400, xy401), xy41), bc, bd) → new_deleteBy0(xy41, xy400, xy401, xy30, xy31, new_asAs(new_esEs5(xy30, xy400, bc), new_esEs4(xy31, xy401, bd)), bc, bd)
new_deleteBy0(xy25, xy26, xy27, xy28, xy29, False, ba, bb) → new_deleteBy(@2(xy28, xy29), xy25, ba, bb)

The TRS R consists of the following rules:

new_esEs7(Just(xy310), Just(xy4010), app(ty_Maybe, ca)) → new_esEs7(xy310, xy4010, ca)
new_esEs22(xy310, xy4010, ty_Integer) → new_esEs14(xy310, xy4010)
new_esEs20(xy312, xy4012, app(ty_Maybe, dg)) → new_esEs7(xy312, xy4012, dg)
new_esEs24(xy311, xy4011, app(ty_Ratio, beb)) → new_esEs15(xy311, xy4011, beb)
new_primPlusNat1(Succ(xy4400), Succ(xy4010000)) → Succ(Succ(new_primPlusNat1(xy4400, xy4010000)))
new_primEqInt(Neg(Succ(xy3100)), Pos(xy4010)) → False
new_primEqInt(Pos(Succ(xy3100)), Neg(xy4010)) → False
new_esEs7(Nothing, Just(xy4010), be) → False
new_esEs7(Just(xy310), Nothing, be) → False
new_esEs13(False, True) → False
new_esEs13(True, False) → False
new_esEs25(xy310, xy4010, ty_Ordering) → new_esEs6(xy310, xy4010)
new_esEs18(Left(xy310), Left(xy4010), app(app(ty_Either, baa), bab), hc) → new_esEs18(xy310, xy4010, baa, bab)
new_esEs24(xy311, xy4011, app(app(ty_Either, bec), bed)) → new_esEs18(xy311, xy4011, bec, bed)
new_primEqInt(Neg(Zero), Pos(Succ(xy40100))) → False
new_primEqInt(Pos(Zero), Neg(Succ(xy40100))) → False
new_esEs18(Left(xy310), Left(xy4010), app(ty_Maybe, hg), hc) → new_esEs7(xy310, xy4010, hg)
new_esEs18(Right(xy310), Right(xy4010), baf, ty_@0) → new_esEs17(xy310, xy4010)
new_esEs21(xy311, xy4011, ty_Char) → new_esEs11(xy311, xy4011)
new_esEs8(Float(xy310, xy311), Float(xy4010, xy4011)) → new_esEs16(new_sr(xy310, xy4010), new_sr(xy311, xy4011))
new_esEs7(Just(xy310), Just(xy4010), ty_Double) → new_esEs9(xy310, xy4010)
new_esEs5(xy30, xy400, app(ty_[], bgb)) → new_esEs10(xy30, xy400, bgb)
new_esEs21(xy311, xy4011, ty_@0) → new_esEs17(xy311, xy4011)
new_primMulNat0(Zero, Zero) → Zero
new_esEs5(xy30, xy400, ty_Int) → new_esEs16(xy30, xy400)
new_esEs23(xy310, xy4010, ty_Ordering) → new_esEs6(xy310, xy4010)
new_esEs4(xy31, xy401, app(ty_Maybe, be)) → new_esEs7(xy31, xy401, be)
new_esEs22(xy310, xy4010, app(app(ty_Either, gf), gg)) → new_esEs18(xy310, xy4010, gf, gg)
new_esEs7(Just(xy310), Just(xy4010), app(app(app(ty_@3, ce), cf), cg)) → new_esEs19(xy310, xy4010, ce, cf, cg)
new_esEs18(Right(xy310), Right(xy4010), baf, app(ty_Ratio, bbc)) → new_esEs15(xy310, xy4010, bbc)
new_esEs21(xy311, xy4011, ty_Integer) → new_esEs14(xy311, xy4011)
new_esEs18(Left(xy310), Left(xy4010), ty_Double, hc) → new_esEs9(xy310, xy4010)
new_esEs5(xy30, xy400, ty_Double) → new_esEs9(xy30, xy400)
new_esEs24(xy311, xy4011, ty_Double) → new_esEs9(xy311, xy4011)
new_esEs21(xy311, xy4011, app(ty_[], ef)) → new_esEs10(xy311, xy4011, ef)
new_primPlusNat0(Zero, xy401000) → Succ(xy401000)
new_esEs23(xy310, xy4010, ty_Double) → new_esEs9(xy310, xy4010)
new_esEs23(xy310, xy4010, app(app(ty_@2, bcc), bcd)) → new_esEs12(xy310, xy4010, bcc, bcd)
new_esEs22(xy310, xy4010, ty_@0) → new_esEs17(xy310, xy4010)
new_esEs4(xy31, xy401, ty_Char) → new_esEs11(xy31, xy401)
new_sr(Pos(xy3100), Neg(xy40100)) → Neg(new_primMulNat0(xy3100, xy40100))
new_sr(Neg(xy3100), Pos(xy40100)) → Neg(new_primMulNat0(xy3100, xy40100))
new_esEs24(xy311, xy4011, ty_Bool) → new_esEs13(xy311, xy4011)
new_esEs18(Left(xy310), Left(xy4010), ty_Bool, hc) → new_esEs13(xy310, xy4010)
new_esEs23(xy310, xy4010, app(ty_[], bcb)) → new_esEs10(xy310, xy4010, bcb)
new_esEs21(xy311, xy4011, app(ty_Ratio, fb)) → new_esEs15(xy311, xy4011, fb)
new_esEs24(xy311, xy4011, app(app(app(ty_@3, bee), bef), beg)) → new_esEs19(xy311, xy4011, bee, bef, beg)
new_esEs22(xy310, xy4010, ty_Char) → new_esEs11(xy310, xy4010)
new_esEs20(xy312, xy4012, ty_Float) → new_esEs8(xy312, xy4012)
new_esEs5(xy30, xy400, app(app(ty_Either, bgg), bgh)) → new_esEs18(xy30, xy400, bgg, bgh)
new_esEs21(xy311, xy4011, app(ty_Maybe, fa)) → new_esEs7(xy311, xy4011, fa)
new_esEs7(Just(xy310), Just(xy4010), ty_Integer) → new_esEs14(xy310, xy4010)
new_esEs4(xy31, xy401, app(app(app(ty_@3, da), db), dc)) → new_esEs19(xy31, xy401, da, db, dc)
new_esEs24(xy311, xy4011, ty_@0) → new_esEs17(xy311, xy4011)
new_esEs20(xy312, xy4012, app(app(ty_@2, de), df)) → new_esEs12(xy312, xy4012, de, df)
new_esEs18(Left(xy310), Left(xy4010), ty_Ordering, hc) → new_esEs6(xy310, xy4010)
new_esEs20(xy312, xy4012, ty_Char) → new_esEs11(xy312, xy4012)
new_esEs26(xy311, xy4011, ty_Integer) → new_esEs14(xy311, xy4011)
new_esEs18(Right(xy310), Right(xy4010), baf, ty_Double) → new_esEs9(xy310, xy4010)
new_esEs23(xy310, xy4010, ty_Bool) → new_esEs13(xy310, xy4010)
new_esEs18(Left(xy310), Left(xy4010), app(app(ty_@2, he), hf), hc) → new_esEs12(xy310, xy4010, he, hf)
new_esEs5(xy30, xy400, ty_Integer) → new_esEs14(xy30, xy400)
new_esEs18(Right(xy310), Right(xy4010), baf, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs19(xy310, xy4010, bbf, bbg, bbh)
new_esEs25(xy310, xy4010, ty_Bool) → new_esEs13(xy310, xy4010)
new_primEqNat0(Zero, Succ(xy40100)) → False
new_primEqNat0(Succ(xy3100), Zero) → False
new_esEs21(xy311, xy4011, app(app(app(ty_@3, ff), fg), fh)) → new_esEs19(xy311, xy4011, ff, fg, fh)
new_esEs25(xy310, xy4010, ty_Double) → new_esEs9(xy310, xy4010)
new_esEs17(@0, @0) → True
new_esEs5(xy30, xy400, app(ty_Maybe, bge)) → new_esEs7(xy30, xy400, bge)
new_esEs25(xy310, xy4010, app(ty_[], beh)) → new_esEs10(xy310, xy4010, beh)
new_esEs20(xy312, xy4012, app(ty_[], dd)) → new_esEs10(xy312, xy4012, dd)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs22(xy310, xy4010, app(app(app(ty_@3, gh), ha), hb)) → new_esEs19(xy310, xy4010, gh, ha, hb)
new_esEs22(xy310, xy4010, app(ty_Ratio, ge)) → new_esEs15(xy310, xy4010, ge)
new_esEs7(Just(xy310), Just(xy4010), app(ty_Ratio, cb)) → new_esEs15(xy310, xy4010, cb)
new_esEs25(xy310, xy4010, ty_Char) → new_esEs11(xy310, xy4010)
new_esEs4(xy31, xy401, app(ty_[], bca)) → new_esEs10(xy31, xy401, bca)
new_esEs25(xy310, xy4010, ty_Float) → new_esEs8(xy310, xy4010)
new_esEs20(xy312, xy4012, ty_Int) → new_esEs16(xy312, xy4012)
new_esEs4(xy31, xy401, app(ty_Ratio, bhd)) → new_esEs15(xy31, xy401, bhd)
new_esEs20(xy312, xy4012, ty_Ordering) → new_esEs6(xy312, xy4012)
new_esEs26(xy311, xy4011, ty_Int) → new_esEs16(xy311, xy4011)
new_esEs5(xy30, xy400, ty_Bool) → new_esEs13(xy30, xy400)
new_esEs6(GT, LT) → False
new_esEs6(LT, GT) → False
new_esEs24(xy311, xy4011, app(ty_Maybe, bea)) → new_esEs7(xy311, xy4011, bea)
new_esEs5(xy30, xy400, ty_@0) → new_esEs17(xy30, xy400)
new_esEs23(xy310, xy4010, app(ty_Maybe, bce)) → new_esEs7(xy310, xy4010, bce)
new_esEs25(xy310, xy4010, ty_Int) → new_esEs16(xy310, xy4010)
new_esEs25(xy310, xy4010, ty_Integer) → new_esEs14(xy310, xy4010)
new_esEs21(xy311, xy4011, app(app(ty_@2, eg), eh)) → new_esEs12(xy311, xy4011, eg, eh)
new_esEs21(xy311, xy4011, app(app(ty_Either, fc), fd)) → new_esEs18(xy311, xy4011, fc, fd)
new_esEs14(Integer(xy310), Integer(xy4010)) → new_primEqInt(xy310, xy4010)
new_esEs10(:(xy310, xy311), :(xy4010, xy4011), bca) → new_asAs(new_esEs23(xy310, xy4010, bca), new_esEs10(xy311, xy4011, bca))
new_esEs4(xy31, xy401, ty_Integer) → new_esEs14(xy31, xy401)
new_esEs7(Just(xy310), Just(xy4010), app(app(ty_Either, cc), cd)) → new_esEs18(xy310, xy4010, cc, cd)
new_esEs18(Right(xy310), Right(xy4010), baf, ty_Ordering) → new_esEs6(xy310, xy4010)
new_esEs18(Right(xy310), Right(xy4010), baf, ty_Float) → new_esEs8(xy310, xy4010)
new_esEs11(Char(xy310), Char(xy4010)) → new_primEqNat0(xy310, xy4010)
new_esEs25(xy310, xy4010, app(ty_Maybe, bfc)) → new_esEs7(xy310, xy4010, bfc)
new_esEs24(xy311, xy4011, app(ty_[], bdf)) → new_esEs10(xy311, xy4011, bdf)
new_esEs7(Just(xy310), Just(xy4010), ty_Float) → new_esEs8(xy310, xy4010)
new_esEs23(xy310, xy4010, app(ty_Ratio, bcf)) → new_esEs15(xy310, xy4010, bcf)
new_esEs18(Right(xy310), Right(xy4010), baf, app(ty_Maybe, bbb)) → new_esEs7(xy310, xy4010, bbb)
new_esEs21(xy311, xy4011, ty_Double) → new_esEs9(xy311, xy4011)
new_esEs18(Left(xy310), Left(xy4010), ty_Float, hc) → new_esEs8(xy310, xy4010)
new_esEs24(xy311, xy4011, app(app(ty_@2, bdg), bdh)) → new_esEs12(xy311, xy4011, bdg, bdh)
new_esEs18(Left(xy310), Left(xy4010), ty_Int, hc) → new_esEs16(xy310, xy4010)
new_esEs20(xy312, xy4012, app(app(app(ty_@3, ec), ed), ee)) → new_esEs19(xy312, xy4012, ec, ed, ee)
new_sr(Neg(xy3100), Neg(xy40100)) → Pos(new_primMulNat0(xy3100, xy40100))
new_esEs24(xy311, xy4011, ty_Char) → new_esEs11(xy311, xy4011)
new_esEs5(xy30, xy400, app(ty_Ratio, bgf)) → new_esEs15(xy30, xy400, bgf)
new_esEs4(xy31, xy401, ty_Float) → new_esEs8(xy31, xy401)
new_asAs(False, xy43) → False
new_sr(Pos(xy3100), Pos(xy40100)) → Pos(new_primMulNat0(xy3100, xy40100))
new_esEs18(Right(xy310), Right(xy4010), baf, app(app(ty_@2, bah), bba)) → new_esEs12(xy310, xy4010, bah, bba)
new_esEs24(xy311, xy4011, ty_Int) → new_esEs16(xy311, xy4011)
new_primEqNat0(Zero, Zero) → True
new_esEs18(Left(xy310), Left(xy4010), ty_Char, hc) → new_esEs11(xy310, xy4010)
new_esEs15(:%(xy310, xy311), :%(xy4010, xy4011), bhd) → new_asAs(new_esEs27(xy310, xy4010, bhd), new_esEs26(xy311, xy4011, bhd))
new_esEs25(xy310, xy4010, app(app(ty_@2, bfa), bfb)) → new_esEs12(xy310, xy4010, bfa, bfb)
new_primMulNat0(Zero, Succ(xy401000)) → Zero
new_primMulNat0(Succ(xy31000), Zero) → Zero
new_esEs21(xy311, xy4011, ty_Bool) → new_esEs13(xy311, xy4011)
new_esEs21(xy311, xy4011, ty_Int) → new_esEs16(xy311, xy4011)
new_esEs20(xy312, xy4012, app(ty_Ratio, dh)) → new_esEs15(xy312, xy4012, dh)
new_esEs18(Right(xy310), Right(xy4010), baf, app(app(ty_Either, bbd), bbe)) → new_esEs18(xy310, xy4010, bbd, bbe)
new_esEs22(xy310, xy4010, app(ty_[], ga)) → new_esEs10(xy310, xy4010, ga)
new_esEs20(xy312, xy4012, ty_Bool) → new_esEs13(xy312, xy4012)
new_esEs25(xy310, xy4010, app(app(ty_Either, bfe), bff)) → new_esEs18(xy310, xy4010, bfe, bff)
new_esEs5(xy30, xy400, app(app(ty_@2, bgc), bgd)) → new_esEs12(xy30, xy400, bgc, bgd)
new_esEs4(xy31, xy401, ty_Int) → new_esEs16(xy31, xy401)
new_esEs18(Right(xy310), Left(xy4010), baf, hc) → False
new_esEs18(Left(xy310), Right(xy4010), baf, hc) → False
new_esEs13(False, False) → True
new_esEs4(xy31, xy401, ty_Double) → new_esEs9(xy31, xy401)
new_esEs5(xy30, xy400, app(app(app(ty_@3, bha), bhb), bhc)) → new_esEs19(xy30, xy400, bha, bhb, bhc)
new_esEs4(xy31, xy401, ty_Bool) → new_esEs13(xy31, xy401)
new_esEs22(xy310, xy4010, ty_Double) → new_esEs9(xy310, xy4010)
new_primPlusNat0(Succ(xy440), xy401000) → Succ(Succ(new_primPlusNat1(xy440, xy401000)))
new_esEs22(xy310, xy4010, ty_Float) → new_esEs8(xy310, xy4010)
new_esEs7(Just(xy310), Just(xy4010), app(ty_[], bf)) → new_esEs10(xy310, xy4010, bf)
new_esEs23(xy310, xy4010, ty_Int) → new_esEs16(xy310, xy4010)
new_esEs18(Right(xy310), Right(xy4010), baf, ty_Int) → new_esEs16(xy310, xy4010)
new_esEs20(xy312, xy4012, ty_Integer) → new_esEs14(xy312, xy4012)
new_esEs21(xy311, xy4011, ty_Ordering) → new_esEs6(xy311, xy4011)
new_esEs24(xy311, xy4011, ty_Integer) → new_esEs14(xy311, xy4011)
new_esEs27(xy310, xy4010, ty_Int) → new_esEs16(xy310, xy4010)
new_esEs18(Right(xy310), Right(xy4010), baf, ty_Integer) → new_esEs14(xy310, xy4010)
new_primEqInt(Neg(Succ(xy3100)), Neg(Succ(xy40100))) → new_primEqNat0(xy3100, xy40100)
new_esEs25(xy310, xy4010, app(app(app(ty_@3, bfg), bfh), bga)) → new_esEs19(xy310, xy4010, bfg, bfh, bga)
new_esEs7(Just(xy310), Just(xy4010), ty_Int) → new_esEs16(xy310, xy4010)
new_esEs20(xy312, xy4012, app(app(ty_Either, ea), eb)) → new_esEs18(xy312, xy4012, ea, eb)
new_esEs18(Left(xy310), Left(xy4010), ty_Integer, hc) → new_esEs14(xy310, xy4010)
new_primPlusNat1(Zero, Succ(xy4010000)) → Succ(xy4010000)
new_primPlusNat1(Succ(xy4400), Zero) → Succ(xy4400)
new_esEs6(GT, GT) → True
new_esEs6(GT, EQ) → False
new_esEs6(EQ, GT) → False
new_esEs16(xy31, xy401) → new_primEqInt(xy31, xy401)
new_esEs18(Left(xy310), Left(xy4010), app(ty_Ratio, hh), hc) → new_esEs15(xy310, xy4010, hh)
new_esEs5(xy30, xy400, ty_Ordering) → new_esEs6(xy30, xy400)
new_esEs4(xy31, xy401, app(app(ty_@2, bdd), bde)) → new_esEs12(xy31, xy401, bdd, bde)
new_esEs18(Left(xy310), Left(xy4010), app(ty_[], hd), hc) → new_esEs10(xy310, xy4010, hd)
new_esEs6(EQ, EQ) → True
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs23(xy310, xy4010, app(app(app(ty_@3, bda), bdb), bdc)) → new_esEs19(xy310, xy4010, bda, bdb, bdc)
new_esEs23(xy310, xy4010, ty_Char) → new_esEs11(xy310, xy4010)
new_esEs23(xy310, xy4010, app(app(ty_Either, bcg), bch)) → new_esEs18(xy310, xy4010, bcg, bch)
new_esEs25(xy310, xy4010, app(ty_Ratio, bfd)) → new_esEs15(xy310, xy4010, bfd)
new_primEqInt(Neg(Zero), Neg(Succ(xy40100))) → False
new_primEqInt(Neg(Succ(xy3100)), Neg(Zero)) → False
new_esEs5(xy30, xy400, ty_Float) → new_esEs8(xy30, xy400)
new_esEs18(Right(xy310), Right(xy4010), baf, app(ty_[], bag)) → new_esEs10(xy310, xy4010, bag)
new_esEs21(xy311, xy4011, ty_Float) → new_esEs8(xy311, xy4011)
new_esEs23(xy310, xy4010, ty_Float) → new_esEs8(xy310, xy4010)
new_esEs18(Right(xy310), Right(xy4010), baf, ty_Bool) → new_esEs13(xy310, xy4010)
new_esEs20(xy312, xy4012, ty_@0) → new_esEs17(xy312, xy4012)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs24(xy311, xy4011, ty_Float) → new_esEs8(xy311, xy4011)
new_esEs27(xy310, xy4010, ty_Integer) → new_esEs14(xy310, xy4010)
new_esEs18(Left(xy310), Left(xy4010), app(app(app(ty_@3, bac), bad), bae), hc) → new_esEs19(xy310, xy4010, bac, bad, bae)
new_esEs22(xy310, xy4010, app(app(ty_@2, gb), gc)) → new_esEs12(xy310, xy4010, gb, gc)
new_asAs(True, xy43) → xy43
new_esEs23(xy310, xy4010, ty_Integer) → new_esEs14(xy310, xy4010)
new_esEs10([], :(xy4010, xy4011), bca) → False
new_esEs10(:(xy310, xy311), [], bca) → False
new_primMulNat0(Succ(xy31000), Succ(xy401000)) → new_primPlusNat0(new_primMulNat0(xy31000, Succ(xy401000)), xy401000)
new_esEs20(xy312, xy4012, ty_Double) → new_esEs9(xy312, xy4012)
new_esEs25(xy310, xy4010, ty_@0) → new_esEs17(xy310, xy4010)
new_esEs13(True, True) → True
new_esEs24(xy311, xy4011, ty_Ordering) → new_esEs6(xy311, xy4011)
new_primEqInt(Pos(Succ(xy3100)), Pos(Succ(xy40100))) → new_primEqNat0(xy3100, xy40100)
new_esEs7(Just(xy310), Just(xy4010), ty_@0) → new_esEs17(xy310, xy4010)
new_esEs18(Right(xy310), Right(xy4010), baf, ty_Char) → new_esEs11(xy310, xy4010)
new_esEs12(@2(xy310, xy311), @2(xy4010, xy4011), bdd, bde) → new_asAs(new_esEs25(xy310, xy4010, bdd), new_esEs24(xy311, xy4011, bde))
new_esEs22(xy310, xy4010, ty_Bool) → new_esEs13(xy310, xy4010)
new_esEs4(xy31, xy401, ty_@0) → new_esEs17(xy31, xy401)
new_esEs22(xy310, xy4010, ty_Ordering) → new_esEs6(xy310, xy4010)
new_esEs6(EQ, LT) → False
new_esEs6(LT, EQ) → False
new_esEs10([], [], bca) → True
new_primEqNat0(Succ(xy3100), Succ(xy40100)) → new_primEqNat0(xy3100, xy40100)
new_esEs7(Just(xy310), Just(xy4010), ty_Bool) → new_esEs13(xy310, xy4010)
new_esEs9(Double(xy310, xy311), Double(xy4010, xy4011)) → new_esEs16(new_sr(xy310, xy4010), new_sr(xy311, xy4011))
new_esEs7(Just(xy310), Just(xy4010), app(app(ty_@2, bg), bh)) → new_esEs12(xy310, xy4010, bg, bh)
new_esEs7(Just(xy310), Just(xy4010), ty_Char) → new_esEs11(xy310, xy4010)
new_esEs4(xy31, xy401, ty_Ordering) → new_esEs6(xy31, xy401)
new_esEs7(Just(xy310), Just(xy4010), ty_Ordering) → new_esEs6(xy310, xy4010)
new_esEs18(Left(xy310), Left(xy4010), ty_@0, hc) → new_esEs17(xy310, xy4010)
new_esEs7(Nothing, Nothing, be) → True
new_primEqInt(Pos(Zero), Pos(Succ(xy40100))) → False
new_primEqInt(Pos(Succ(xy3100)), Pos(Zero)) → False
new_esEs6(LT, LT) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs22(xy310, xy4010, app(ty_Maybe, gd)) → new_esEs7(xy310, xy4010, gd)
new_esEs4(xy31, xy401, app(app(ty_Either, baf), hc)) → new_esEs18(xy31, xy401, baf, hc)
new_esEs23(xy310, xy4010, ty_@0) → new_esEs17(xy310, xy4010)
new_esEs5(xy30, xy400, ty_Char) → new_esEs11(xy30, xy400)
new_esEs19(@3(xy310, xy311, xy312), @3(xy4010, xy4011, xy4012), da, db, dc) → new_asAs(new_esEs22(xy310, xy4010, da), new_asAs(new_esEs21(xy311, xy4011, db), new_esEs20(xy312, xy4012, dc)))
new_esEs22(xy310, xy4010, ty_Int) → new_esEs16(xy310, xy4010)

The set Q consists of the following terms:

new_esEs4(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Float)
new_esEs7(Just(x0), Just(x1), ty_Float)
new_esEs25(x0, x1, ty_Bool)
new_esEs16(x0, x1)
new_esEs23(x0, x1, ty_Bool)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs14(Integer(x0), Integer(x1))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_sr(Pos(x0), Pos(x1))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat1(Succ(x0), Zero)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs18(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs7(Just(x0), Just(x1), ty_Ordering)
new_esEs23(x0, x1, ty_Float)
new_esEs4(x0, x1, ty_Double)
new_esEs7(Just(x0), Just(x1), app(ty_[], x2))
new_esEs6(GT, LT)
new_esEs6(LT, GT)
new_esEs25(x0, x1, ty_Char)
new_esEs18(Left(x0), Left(x1), ty_Int, x2)
new_primPlusNat0(Zero, x0)
new_esEs22(x0, x1, ty_@0)
new_esEs18(Right(x0), Right(x1), x2, ty_Double)
new_esEs20(x0, x1, ty_Char)
new_esEs18(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs18(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs6(EQ, LT)
new_esEs6(LT, EQ)
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs7(Just(x0), Nothing, x1)
new_esEs5(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(ty_[], x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs21(x0, x1, ty_Char)
new_esEs18(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs25(x0, x1, ty_Float)
new_esEs6(EQ, EQ)
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Ordering)
new_esEs7(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs7(Just(x0), Just(x1), ty_Double)
new_esEs6(LT, LT)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_Bool)
new_esEs21(x0, x1, ty_@0)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs23(x0, x1, ty_@0)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs8(Float(x0, x1), Float(x2, x3))
new_esEs18(Left(x0), Left(x1), ty_Bool, x2)
new_esEs22(x0, x1, ty_Int)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs18(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs7(Just(x0), Just(x1), ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs7(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_primPlusNat1(Zero, Succ(x0))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs7(Just(x0), Just(x1), ty_Integer)
new_esEs9(Double(x0, x1), Double(x2, x3))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_@0)
new_primMulNat0(Zero, Succ(x0))
new_esEs18(Right(x0), Right(x1), x2, ty_Int)
new_esEs25(x0, x1, ty_Ordering)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs7(Nothing, Just(x0), x1)
new_esEs10([], :(x0, x1), x2)
new_esEs4(x0, x1, ty_Ordering)
new_esEs18(Left(x0), Left(x1), ty_Ordering, x2)
new_primEqNat0(Zero, Zero)
new_esEs22(x0, x1, ty_Ordering)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Float)
new_esEs18(Right(x0), Right(x1), x2, ty_Integer)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs18(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs18(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs24(x0, x1, ty_Bool)
new_esEs18(Left(x0), Left(x1), ty_Char, x2)
new_asAs(True, x0)
new_primMulNat0(Succ(x0), Zero)
new_esEs23(x0, x1, ty_Char)
new_primPlusNat0(Succ(x0), x1)
new_esEs25(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(GT, GT)
new_esEs5(x0, x1, ty_Double)
new_esEs22(x0, x1, ty_Char)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Zero, Zero)
new_esEs13(False, False)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs7(Nothing, Nothing, x0)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(True, False)
new_esEs13(False, True)
new_esEs6(EQ, GT)
new_esEs6(GT, EQ)
new_esEs18(Right(x0), Right(x1), x2, ty_Char)
new_esEs5(x0, x1, ty_@0)
new_esEs27(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Int)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs18(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs18(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs24(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_Bool)
new_esEs10(:(x0, x1), [], x2)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Float)
new_esEs15(:%(x0, x1), :%(x2, x3), x4)
new_esEs24(x0, x1, ty_Double)
new_esEs24(x0, x1, ty_Char)
new_esEs18(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs13(True, True)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs18(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs18(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Ordering)
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, ty_Bool)
new_esEs11(Char(x0), Char(x1))
new_esEs12(@2(x0, x1), @2(x2, x3), x4, x5)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs18(Left(x0), Left(x1), ty_Double, x2)
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Integer)
new_sr(Neg(x0), Neg(x1))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Int)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, ty_Int)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Double)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Double)
new_esEs18(Left(x0), Left(x1), ty_Integer, x2)
new_esEs24(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Float)
new_esEs7(Just(x0), Just(x1), ty_Char)
new_esEs7(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs7(Just(x0), Just(x1), ty_@0)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, ty_Float)
new_esEs7(Just(x0), Just(x1), ty_Bool)
new_primEqNat0(Succ(x0), Zero)
new_esEs24(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs7(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Int)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs18(Left(x0), Right(x1), x2, x3)
new_esEs18(Right(x0), Left(x1), x2, x3)
new_esEs7(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Double)
new_esEs5(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_Bool)
new_primPlusNat1(Zero, Zero)
new_esEs18(Right(x0), Right(x1), x2, ty_Bool)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, ty_Ordering)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_primEqNat0(Zero, Succ(x0))
new_esEs23(x0, x1, ty_Ordering)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_Char)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_Double)
new_esEs27(x0, x1, ty_Integer)
new_esEs18(Right(x0), Right(x1), x2, ty_@0)
new_esEs10([], [], x0)
new_esEs10(:(x0, x1), :(x2, x3), x4)
new_esEs4(x0, x1, ty_Char)
new_esEs18(Left(x0), Left(x1), ty_Float, x2)
new_esEs5(x0, x1, ty_Float)
new_esEs4(x0, x1, ty_Integer)
new_esEs19(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs17(@0, @0)
new_esEs18(Right(x0), Right(x1), x2, ty_Float)
new_asAs(False, x0)
new_esEs20(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_Double)
new_esEs18(Left(x0), Left(x1), ty_@0, x2)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs5(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Int)
new_esEs18(Right(x0), Right(x1), x2, app(ty_[], x3))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: